(directed enhancement of homotopy type theory with types behaving like -categories)
Segal types are the (infinity,1)-categorical version of precategories in simplicial type theory
There are multiple different formalisms of simplicial homotopy type theory; two of them are given in Gratzer, Weinberger, & Buchholtz 2024 and in Riehl & Shulman 2017, and in each formalism there is a different way to define Segal types.
In simplicial homotopy type theory where the directed interval primitive is defined via axioms, let the 2-simplex type be defined as
and let the 2-1-horn type be defined as
where is the propositional truncation of the type . For each type there is a canonical restriction function .
is a Segal type if the restriction function is an equivalence of types.
In simplicial type theory in the type theory with shapes formalism, a Segal type is a type such that given elements , , and and morphisms and , the type
is a contractible type, where is the -simplex probe shape and is its boundary.
Emily Riehl, Michael Shulman, A type theory for synthetic -categories arXiv:1705.07442
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)
Last revised on October 5, 2024 at 17:53:17. See the history of this page for a list of all contributions to it.